% !Mode:: "TeX:UTF-8"

\zhead{Для данной явной спецификации построить эквивалентную неявную спецификацию}

\z \begin{lstlisting}
variable x : Int
value f: Int -> write any Int
      f(t) is ( x := t; x )
\end{lstlisting}

\z \begin{lstlisting}
variable x : Int
value f: Int -> write any Int
      f(t) is ( if x = t then x else t end )
\end{lstlisting}

\z \begin{lstlisting}
variable x : Int
value f: Int >< Int -> write any Unit
  f(u,v) is (if u>v then x:=u else x:=v end)
\end{lstlisting}

\z \begin{lstlisting}
variable x : Int
value f: Int -> write any Int
      f(t) is ( x := t; x := abs x; x )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( x := y; x+t )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( if x = y then x else t end )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write x Int
  f(y) is (x := y; x)
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( y := x; x := t; y-x )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( x := t; x+y )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( y := x; x - 2*t )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( x := t-x; y-x )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( y := x-y; x := x-y; y-x )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( y:=t; y:=x+y; x )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( y:=x; y:=y; x-2*t )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( x:=t-x; x:=t-x; y-x )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( y := x-y; y := x-y; x-y )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( if x > 0 then y := x else x := y end; t )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( if y < x then y := t else x := t end; x )
\end{lstlisting}

\z \begin{lstlisting}
variable x, y : Int
value f: Int -> write any Int
      f(t) is ( if x = t then x := y-1 else x := y+1 end; t )
\end{lstlisting}

\z \begin{lstlisting}
value f : Int >< Int >< Int -> write x,y read z Int >< Int
  f(a,b,c) is if x is 0-y then
       (if c > b+1 then x:=y+1;0-c else x:=y;c end,
        (if a+x < z then 0-c else x:=y+2; b*a end)-x)
           else (y, x:=b; a+b) end
\end{lstlisting}

\z \begin{lstlisting}
value f : Int >< Int -> write x, y, c Int >< Int >< Int
     f (a, b) is local variable v : Int := x in
       for i in <.a+ 1..x .> do v := v+2*(x:=i; y:=x*y; x+i)
            end; (c*b, x:=x-v;a*b, v*v-b*c) end
\end{lstlisting}

\z \begin{lstlisting}
value f : Int >< Int >< Int -> write x, y write z Int >< Int
 f(a,b,c) is if b ~= 0 /\ a \ b = z then
  (if a+b > c+b then y:=(z:=z+1;z);a else a/b end, x:=a*y;
   (if c>y then y:=x+c; x else y:=x-c;0-c end)\b)
     else ( z:=x;x, x:=a+b;z ) end
\end{lstlisting}

\z \begin{lstlisting}
value f : Int >< Int -> write x, y, z Int >< Int >< Int
   f (a, b) is x := 2; local variable v : Int := 1 in
     for i in <. a..a-1 +b.> do
      if x > 0 then v := v+1 end;
        let u = v*v in v := i*(x:=x+u; i)*2 end
          end; (y:= z; a, v:=v+1;x, b+v ) end
\end{lstlisting}

\z \begin{lstlisting}
value f : Int >< Int >< Int -> write x, y, z Int >< Int
  f(a,b,c) is if x ~= y then
    (if a-b < c then y:=b*x; int real b
     elsif a-y>c then x:=a*y; a+y
     else x-y end,
     (a+b)*(if x>0 then c else y:=c+1; 0-c end))
    else (y, x:=a-b;y:=abs x+b;x) end
\end{lstlisting}

\z \begin{lstlisting}
value f : Nat >< Nat >< Int -> write x, y read z, u Int >< Int
   f(a,b,c) is if a+b = z+u => x + y = z+u then
   (if a*y < a*c then y:=z+u;y else x:=y-x+1; c end,
      y*(if x>a then x:=b+y; 0-y else y:=a+b; c end))
      else (y+1, a-z+(x:=x+1;1)) end
\end{lstlisting}



